$\forall$$x$:Id, $T$:Type. normal{-}type\{i:l\}($T$) $\Rightarrow$ normal{-}ds\{i:l\}(fpf{-}single($x$; $T$))